es:ES, A:Type, X:AbsInterface(A). le(X)  AbsInterface(E(X)) 

latex

Definitions

t  T, s = t, x:AB(x), ES, Type, AbsInterface(A), P  Q, , x:A  B(x), P & Q, P  Q, A, e loc e' , x:A. B(x), left + right, Void, case b of inl(x) => s(x) | inr(y) => t(y), P  Q, False, if b then t else f fi , (e <loc e'), let x,y = A in B(x;y), t.1, , (x  l), x  dom(f), A c B, a:A fp B(a), strong-subtype(A;B), E(X), le(X), X(e), e  X, b, P  Q, E, x:A. B(x), x.A(x), can-apply(f;x), do-apply(f;x), Top, outl(x), inr x , f(a), isl(x), <a, b>, x:A.B(x), {x:A| B(x)} , Decision, True, inl x

Lemmas

true wf, false wf, top wf, isl wf, es-E-interface wf, member wf, es-interface wf, event system wf, es-local-le-pred wf, es-local-le-pred-property, assert wf, es-E wf, es-is-interface wf